We generalize the notion of proof term to the realm of transfinite reduction.Proof terms represent reductions in the first-order term format, therebyfacilitating their formal analysis. We show that any transfinite reduction canbe faithfully represented as an infinitary proof term, which is unique up to,infinitary, associativity. Our main use of proof terms is in a definition of permutation equivalence fortransfinite reductions, on the basis of permutation equations. This definitioninvolves a variant of equational logic, adapted for dealing with infiniteobjects. A proof of the compression property via proof terms is presented, whichestablishes permutation equivalence between the original and the compressedreductions.
展开▼
